Automatic Generation of Classification Theorems for Finite Algebras
Identifieur interne : 006C34 ( Main/Exploration ); précédent : 006C33; suivant : 006C35Automatic Generation of Classification Theorems for Finite Algebras
Auteurs : Simon Colton [Royaume-Uni] ; Andreas Meier [Allemagne] ; Volker Sorge [Royaume-Uni] ; Roy Mccasland [Royaume-Uni]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: Classifying finite algebraic structures has been a major motivation behind much research in pure mathematics. Automated techniques have aided in this process, but this has largely been at a quantitative level. In contrast, we present a qualitative approach which produces verified theorems, which classify algebras of a particular type and size into isomorphism classes. We describe both a semi-automated and a fully automated bootstrapping approach to building and verifying classification theorems. In the latter case, we have implemented a procedure which takes the axioms of the algebra and produces a decision tree embedding a fully verified classification theorem. This has been achieved by the integration (and improvement) of a number of automated reasoning techniques: we use the Mace model generator, the HR and C4.5 machine learning systems, the Spass theorem prover, and the Gap computer algebra system to reduce the complexity of the problems given to Spass. We demonstrate the power of this approach by classifying loops, groups, monoids and quasigroups of various sizes.
Url:
DOI: 10.1007/978-3-540-25984-8_30
Affiliations:
- Allemagne, Royaume-Uni
- Angleterre, Grand Londres, Midlands de l'Ouest, Sarre (Land), Écosse
- Birmingham, Londres, Sarrebruck, Édimbourg
- Université d'Édimbourg, Université de Birmingham
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 003B59
- to stream Istex, to step Curation: 003B15
- to stream Istex, to step Checkpoint: 001843
- to stream Main, to step Merge: 006F38
- to stream Main, to step Curation: 006C34
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Automatic Generation of Classification Theorems for Finite Algebras</title><author><name sortKey="Colton, Simon" sort="Colton, Simon" uniqKey="Colton S" first="Simon" last="Colton">Simon Colton</name></author><author><name sortKey="Meier, Andreas" sort="Meier, Andreas" uniqKey="Meier A" first="Andreas" last="Meier">Andreas Meier</name></author><author><name sortKey="Sorge, Volker" sort="Sorge, Volker" uniqKey="Sorge V" first="Volker" last="Sorge">Volker Sorge</name></author><author><name sortKey="Mccasland, Roy" sort="Mccasland, Roy" uniqKey="Mccasland R" first="Roy" last="Mccasland">Roy Mccasland</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:F8A899C6272C5D7ADFA45E5C4E388007FE3AC8AB</idno><date when="2004" year="2004">2004</date><idno type="doi">10.1007/978-3-540-25984-8_30</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-VLD1X817-N/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003B59</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003B59</idno><idno type="wicri:Area/Istex/Curation">003B15</idno><idno type="wicri:Area/Istex/Checkpoint">001843</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001843</idno><idno type="wicri:doubleKey">0302-9743:2004:Colton S:automatic:generation:of</idno><idno type="wicri:Area/Main/Merge">006F38</idno><idno type="wicri:Area/Main/Curation">006C34</idno><idno type="wicri:Area/Main/Exploration">006C34</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Automatic Generation of Classification Theorems for Finite Algebras</title><author><name sortKey="Colton, Simon" sort="Colton, Simon" uniqKey="Colton S" first="Simon" last="Colton">Simon Colton</name><affiliation wicri:level="3"><country xml:lang="fr">Royaume-Uni</country><wicri:regionArea>Department of Computing, Imperial College, London</wicri:regionArea><placeName><settlement type="city">Londres</settlement><region type="country">Angleterre</region><region type="région" nuts="1">Grand Londres</region></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Royaume-Uni</country></affiliation></author><author><name sortKey="Meier, Andreas" sort="Meier, Andreas" uniqKey="Meier A" first="Andreas" last="Meier">Andreas Meier</name><affiliation wicri:level="3"><country xml:lang="fr">Allemagne</country><wicri:regionArea>DFKI GmbH, Saarbrücken</wicri:regionArea><placeName><region type="land" nuts="2">Sarre (Land)</region><settlement type="city">Sarrebruck</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Allemagne</country></affiliation></author><author><name sortKey="Sorge, Volker" sort="Sorge, Volker" uniqKey="Sorge V" first="Volker" last="Sorge">Volker Sorge</name><affiliation wicri:level="4"><country xml:lang="fr">Royaume-Uni</country><wicri:regionArea>School of Computer Science, University of Birmingham</wicri:regionArea><placeName><settlement type="city">Birmingham</settlement><region type="country">Angleterre</region><region type="région" nuts="1">Midlands de l'Ouest</region></placeName><orgName type="university">Université de Birmingham</orgName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Royaume-Uni</country></affiliation></author><author><name sortKey="Mccasland, Roy" sort="Mccasland, Roy" uniqKey="Mccasland R" first="Roy" last="Mccasland">Roy Mccasland</name><affiliation wicri:level="4"><country xml:lang="fr">Royaume-Uni</country><wicri:regionArea>School of Informatics, University of Edinburgh</wicri:regionArea><placeName><settlement type="city">Édimbourg</settlement><region type="country">Écosse</region></placeName><orgName type="university">Université d'Édimbourg</orgName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Royaume-Uni</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: Classifying finite algebraic structures has been a major motivation behind much research in pure mathematics. Automated techniques have aided in this process, but this has largely been at a quantitative level. In contrast, we present a qualitative approach which produces verified theorems, which classify algebras of a particular type and size into isomorphism classes. We describe both a semi-automated and a fully automated bootstrapping approach to building and verifying classification theorems. In the latter case, we have implemented a procedure which takes the axioms of the algebra and produces a decision tree embedding a fully verified classification theorem. This has been achieved by the integration (and improvement) of a number of automated reasoning techniques: we use the Mace model generator, the HR and C4.5 machine learning systems, the Spass theorem prover, and the Gap computer algebra system to reduce the complexity of the problems given to Spass. We demonstrate the power of this approach by classifying loops, groups, monoids and quasigroups of various sizes.</div></front></TEI><affiliations><list><country><li>Allemagne</li><li>Royaume-Uni</li></country><region><li>Angleterre</li><li>Grand Londres</li><li>Midlands de l'Ouest</li><li>Sarre (Land)</li><li>Écosse</li></region><settlement><li>Birmingham</li><li>Londres</li><li>Sarrebruck</li><li>Édimbourg</li></settlement><orgName><li>Université d'Édimbourg</li><li>Université de Birmingham</li></orgName></list><tree><country name="Royaume-Uni"><region name="Angleterre"><name sortKey="Colton, Simon" sort="Colton, Simon" uniqKey="Colton S" first="Simon" last="Colton">Simon Colton</name></region><name sortKey="Colton, Simon" sort="Colton, Simon" uniqKey="Colton S" first="Simon" last="Colton">Simon Colton</name><name sortKey="Mccasland, Roy" sort="Mccasland, Roy" uniqKey="Mccasland R" first="Roy" last="Mccasland">Roy Mccasland</name><name sortKey="Mccasland, Roy" sort="Mccasland, Roy" uniqKey="Mccasland R" first="Roy" last="Mccasland">Roy Mccasland</name><name sortKey="Sorge, Volker" sort="Sorge, Volker" uniqKey="Sorge V" first="Volker" last="Sorge">Volker Sorge</name><name sortKey="Sorge, Volker" sort="Sorge, Volker" uniqKey="Sorge V" first="Volker" last="Sorge">Volker Sorge</name></country><country name="Allemagne"><region name="Sarre (Land)"><name sortKey="Meier, Andreas" sort="Meier, Andreas" uniqKey="Meier A" first="Andreas" last="Meier">Andreas Meier</name></region><name sortKey="Meier, Andreas" sort="Meier, Andreas" uniqKey="Meier A" first="Andreas" last="Meier">Andreas Meier</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 006C34 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 006C34 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:F8A899C6272C5D7ADFA45E5C4E388007FE3AC8AB
|texte= Automatic Generation of Classification Theorems for Finite Algebras
}}
| This area was generated with Dilib version V0.6.33. |  |